Repository navigation
Add(notebook-lean,#20184): ANALYSE-06 Sensibilite 2026 -- carnet FR+_en executes + Check.lean (Pli 2 #19898) - #20392
Conversation
…e 0<3, s=3 contre-intuitif, familles 2026 citees avec statut Ajout additif au lac sensitivity_lean (Pli 2, Epic Origami #19898) : aucun enonce existant modifie. Temoins tribes32 (3 tribus x 2 coordonnees) : - s(0)=0 (decide), bs(0)>=3 (famille des tribus admissible), separation locale stricte (patron orOfAnds, generalisee a 3 blocs) ; - tribes32_sensitivity_eq_three : le majorant naif s<=2 REFUTE par decide a la compilation (sommet une-lampe-par-tribu : s=3) -- le recit 'mesure, pas suppose' du carnet ANALYSE-06 ; - familles openai/math 127/132/186/192 citees avec leur statut dans les docstrings (jamais 'OpenAI a prouve donc X'). lake build SUCCESS (3025 jobs, FR+EN+roots) ; distinct_code_sorry: 0. Sibling _en miroir (namespace Sensitivity_en, imports _en). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…en executes + Check.lean, mesures exactes s/bs Pli 2 (Epic Origami #19898) : carnet ANALYSE-06-Sensibilite-2026-Lean-Python + sibling _en, executes avec outputs (kernel python3). Check.lean (hors globs de la lib) expose signatures + #print axioms pour le carnet. Contenu : - audit pin v4.33.0 : 0 notion dans Mathlib/ propre, Archive/Sensitivity.lean a la racine du paquet (le lac = dust-off autonome de Huang) ; - build reel 3025 jobs + compteur canonique in-notebook (distinct_code_sorry 0 ; avant main 19 fichiers / apres 22, delta = Sens2026 + _en + Check) ; - experiences exactes (DP sous-ensembles pour bs) : mesure = decide chiffre a chiffre ; arc tribes ratio 1 (k=2,3,4) ; addr6 s=3 bs=3 (hypothese d'auteur refutee par la mesure) ; sweep exhaustif n=3 : 0 temoin, n=4 : 24 temoins tous (s,bs)=(2,3) -- la separation globale bs>s nat a n=4 ; - familles 127/132/186/192 openai/math citees avec statut (table 3 statuts, 132 preprint non relu par experts) -- jamais adoptees comme resultats ; - 3 exercices C.1 (stubs executables, aucune erreur volontaire). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
…R (twin-parity STRUCTURE_DRIFT) Le builder nbformat frappait des ids neufs pour le jumeau _en ; la garde twin-parity exige la meme sequence de cell_id. Reconstruit sur base FR : ids/ordre/code/outputs inchanges, seuls les 19 markdown portent la traduction. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Disposition des deux jambes rouges du PR gate (tete 26b58bf, mesure c.429) : 1. twin-parity-guard STRUCTURE_DRIFT — corrige par 144d1b5. Le builder nbformat frappait des 2. check-nav-chain 2 NEW unreachable (
Demande au coordinateur : arbitrage #19076 (a)/(b) ou realignement du baseline cote main ; les liens de citation restent en attendant. |
…itrage #19076 option b, c.6114582529) Entrees ajoutees dans la PR elle-meme (precedent renommages #19482) : les carnets ANALYSE-06 FR/_en citent Lean-12b/12c en liens markdown, ce qui leur donne un inbound et retire leur statut d'entree de serie Lean -- reclassement unreachable documente par l'arbitrage coordinateur. Garde verifiee sur la branche : 0 NEW finding, rc=0. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Path-collision (organ #13359/#13615)Cette PR #20392 (
|
|
[ADJOINT PREFLIGHT] Blocking - check requis en echec. Scripts Tests (CPU) failure (derniere jambe 2026-10-11T22:48:08Z, PR gate 22:47:40Z ne fait que relayer) - scripts/translation/tests/test_check_translation_parity.py::test_full_repo_state_passes_parity - citation exacte du log : translation pair count drifted from the declared perimeter, found 10, declared 9 (update EXPECTED_PAIR_COUNT knowingly - hold i18n #10038). Geste attendu de la lane porteuse : incrementer EXPECTED_PAIR_COUNT 9 vers 10 dans la meme PR (la paire ANALYSE-06 FR + _en est la 10e paire de traduction), laisser les checks se re-agreger - la tete changera, ce dossier perira et un dossier frais sera requis. Pour ai-01 - le seul obstacle est ce compteur. Vert par ailleurs a la tete 9763e6a : ci/Lean CI (sensitivity_lean) success, proof-integrity (sensitivity_lean) success, check-nav-chain SUCCESS (22:53:38Z - le baseline +2 Lean-12b/12c a fait son office, arbitrage c.6114582529 lu a la source et conforme au body a la lettre), H.4 firsthand conforme sur les deux carnets (FR et _en 29 cellules, 10 code, execution_count 1-10, 0 cellule code sans output, 0 erreur, 0 interdit C.1), b0 clear, reviews 0, threads 0. Path-collision advisory faible x6 sur le fichier baseline partage - connu, non bloquant. Lane porteuse myia-ai-01:CoursIA-2 (Grain DEEP/notebook-lean, prev MED/tooling #19786) ; emetteur tiers myia-po-2025:CoursIA-2. Organe --emit --template depuis checkout main isole propre 6ad27f7, rc 3 = BLOCKED derive (diagnostic stderr nomme Scripts Tests CPU). |
…LYSE-06) Le compteur declare du perimetre de traduction passe de 9 a 10 avec l'entree datee de la paire ajoutee par cette PR (SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en). Rouge mesure a tete constante : 1 failed / 34 passed, meme classe que l'entree #19996 (la paire arrive avec son carnet, la declaration l'enregistre dans la meme PR). Post-fix : 35/35. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
[ADJOINT PREFLIGHT] Blocking -- champ Pour ai-01 -- mesures firsthand a la tete dc69092 (worktree detache sur refs/remotes/pr/20392 ; fetch verifie : 9763e6a vers dc69092). H.4 conforme sur les deux carnets AJOUTES par la PR : FR et _en, 29 cellules chacun (19 markdown + 10 code), execution_count 1-10 sur les 10 cellules code, 0 cellule code sans output, 0 sortie d'erreur, 0 motif interdit C.1 (raise NotImplementedError / assert False / 1/0). Les carnets Lean ne s'executent pas localement (tolerance documentee) : les sorties committee sont comptees telles quelles, pas fabriquees. Crible domain = python scripts/notebook_tools/detect_md_content_loss.py --base origin/main --head HEAD : rc=0 et findings=0 sur les deux (FR new_file=true, 19 cellules md / 17915 car. normalises ; _en mode=translation contre le jumeau FR, 19 md / 17792 car.). b0 rc=0 -- aucun nit non leve ; 2 commentaires non evalues lus a la main (disposition de jsboige du 21:38:17Z, deja perimee par la tete ; dossier precedent du 23:29:40Z). reviews 0, threads inline 0. Lane porteuse myia-ai-01:CoursIA-2 (Grain DEEP/notebook-lean, prev MED/tooling #19786) ; emetteur tiers myia-po-2025:CoursIA-2. Organe --emit --template depuis worktree detache sur origin/main 6ad27f7 ; rc 3 = BLOCKED derive, le diagnostic stderr nomme la contradiction de la claim checks sur la jambe PR gate DWELL. |
…e navigation main est rouge sur check-nav-chain depuis l'arrivee de ANALYSE-10 (#20429) et de ANALYSE-06_en (#20392) : deux orphan_entry, aucun carnet ne pointe vers eux. Toute PR dont la voie rapide execute check-nav-chain herite de ce rouge. - ANALYSE-09 : la colonne « Notebook suivant » pointe vers ANALYSE-10 ; le lien vers la version anglaise passe sur sa propre ligne (09_en garde son lien entrant). - ANALYSE-06 : ajout du lien vers sa version anglaise, sur le modele de 09. Markdown seul (cellule de navigation), aucune cellule de code ni sortie modifiee : pas de re-execution due (C.2). Les jumeaux _en ne sont pas touches (translation-guard). check_notebook_nav_chain.py --check : 0 NEW finding (main : 2). Hors flotte : session cloud du mainteneur (exemption #17713). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LRbWZZHE9jZscr8ya3niWA
… parite FR/EN rouge sur main (#20777) * fix(translation,#20551): re-rendu EN de 01-2 GPT-5 Image apres le TP2 -- parite FR/EN de main test_full_repo_state_passes_parity est rouge sur main depuis #20551 (13/10) : le TP2 a ajoute 8 cellules au carnet FR 01-2 et retire la cellule 17aab9f8, sans re-rendre le jumeau _en cree la veille par #20449 (STRUCTURE_DRIFT, 37 cellules FR contre 30 EN). La jambe Scripts Tests de toute PR rougit sur ce seul defaut. Second defaut, muet : 6 cellules markdown deja traduites ont change en FR dans #20551 (exercices devenus exemples guides). La mise a jour du CSV a rafraichi leur src_hash en gardant l'ancien text_en : la synchro les voit IN_SYNC alors que la traduction decrit l'ancien texte. Geste (pipeline T1/T3/T4, aucune edition du carnet _en a la main) : - T1 : CSV deja a jour cote FR ; ligne orpheline 17aab9f8 retiree. - T3 : 10 text_en ecrits (4 nouvelles cellules, 6 cellules modifiees), hash_en = cell_hash du module ; spans code et sorties citees inchanges. - T4 : render --require-translated, 20/20 markdown traduits, 17 code copiees verbatim, 0 fallback, 0 orphelin. Validation : pytest scripts/translation/tests/ -> 403 passed, 2 skipped. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Fix(analyse,nav): rattacher ANALYSE-10 et ANALYSE-06_en a la chaine de navigation main est rouge sur check-nav-chain depuis l'arrivee de ANALYSE-10 (#20429) et de ANALYSE-06_en (#20392) : deux orphan_entry, aucun carnet ne pointe vers eux. Toute PR dont la voie rapide execute check-nav-chain herite de ce rouge. - ANALYSE-09 : la colonne « Notebook suivant » pointe vers ANALYSE-10 ; le lien vers la version anglaise passe sur sa propre ligne (09_en garde son lien entrant). - ANALYSE-06 : ajout du lien vers sa version anglaise, sur le modele de 09. Markdown seul (cellule de navigation), aucune cellule de code ni sortie modifiee : pas de re-execution due (C.2). Les jumeaux _en ne sont pas touches (translation-guard). check_notebook_nav_chain.py --check : 0 NEW finding (main : 2). Hors flotte : session cloud du mainteneur (exemption #17713). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LRbWZZHE9jZscr8ya3niWA * fix(guards,#20777): les organes voient la forme canonique des jumeaux _en Le re-rendu EN de 01-2-GPT-5-Image-Generation rougissait deux gardes sur des faux positifs de detection, pas sur un defaut du carnet : - Split-reading ratchet : le carve-out #17777 (enonce d'exercice adjacent a son stub = forme canonique du depot) ne matchait que le titre francais -- les enonces traduits "### Exercise N" (cellules 31/33 du _en, miroir exact des cellules 31/33 du FR source sur main) tombaient en EXERCISE_READING. Regex etendu a "exerci[cs]e", garde-fous (en-tete d'interpretation cache, citation de sortie) etendus en miroir anglais -- le controle negatif "interpretation deguisee sous titre Exercise" reste rouge. - Plan-loss gate : _BOLD_INLINE_RE exigeait une ligne vide apres le bloc gras -- un label "**Instructions**:" colle a sa liste numerotee etait invisible a la passe SUBSTANCE_FOUND_INLINE_BOLD, d'ou un LOST_SECTION faux positif sur la retrogradation "### Instructions" -> label bold. Le lookahead accepte tout fin de ligne (la queue ne franchit pas \n). Controles : self-test 7/7 ; 159 tests verts dont 3 nouveaux (enonce EN exempte, interpretation deguisee EN signalee, label bold + liste colle trouve) ; cliquet rc=0 et plan-loss rc=0 sur les 3 carnets modifies ; suite translation 403 passed / 2 skipped. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_en arrivee sans enregistrement (PR #19943) (#21383) La 14e paire detectee par discover_pairs() est SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en, mergee le 2026-10-19 (c91ad98) sans mise a jour de la declaration -- le test test_full_repo_state_passes_parity est rouge sur main pur (found 14, declared 13, diagnostic po-2027 dashboard 2026-10-19T06:10Z) et gele toute PR path-filtree scripts/**. Bump + entree d'historique au patron des precedents (#19996/#20392). Validation locale : 35 passed (pytest scripts/translation/tests/). Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
* Add(ci,#21391): EXPECTED_PAIR_COUNT guard at PR time `main` has now turned red for the fourth time because a notebook PR adds a new `*_<lang>.ipynb` pair without bumping the constant `EXPECTED_PAIR_COUNT` in `scripts/translation/tests/test_check_translation_parity.py`. History of the four rouges: #19996, #20392, #20453, #19943 (constant updated in each by a follow-up PR). The test that compares the count (`test_full_repo_state_passes_parity`) lives in `Scripts Tests (CPU)`, filtered on `scripts/**`, so a notebook PR that doesn't touch `scripts/` doesn't even trigger it. `translation-parity.yml` runs only nightly. The invariant "pair added/removed/renamed => constant bumped in the same PR" has no carrier at PR time. This guard is the carrier. Pipeline (pure git, no clone, no kernel): 1. `git diff --name-status -M50% base..head -- 'MyIA.AI.Notebooks/...'` lists notebook A/D/R status (M is ignored). 2. For each A/D/R translation file `*_<lang>.ipynb`, the guard reads the corresponding FR source at head via `git show head:path` (no disk walk). Files that pair are recorded. 3. If the diff adds or destroys at least one pair AND `EXPECTED_PAIR_COUNT` was not modified in the same diff: ROUGE, with the exact line to edit, the new value expected, and the 5-line history-entry pattern already in use by the file. 4. If the diff modified the constant, the new value is compared to `discover_pairs(repo_root, langs)` (the disk walk, only on this branch). ROUGE if the values disagree. Acceptance (re-run on the SHAs cited in the issue): 1. POSITIVE on #19943 (c91ad98^..c91ad98): ROUGE, names `ANALYSE-07-Percolation-Critique_en`, expected bump 13 -> 14. 2. NEGATIVE on #21383 (origin/main..pr-21383): GREEN (no pair diff). 3. M-only diff (existing _en.ipynb modified): GREEN, A/D/R set excludes M by design. 4. .tmp/ orphan on local disk: the guard reads git diff, not disk; the orphan is invisible to it. 5. Cost: 0.35s (no disk count) / 0.35s (with disk count) on this machine; no blob:none clone of 2 GB. 25/25 pytest tests PASSED. Out of scope: the workflow integration lives in `.github/workflows/always-on-guards.yml` -- ai-01 does the merge (claim `paths: scripts/translation/**` only; workflow file excluded). Refs: #21391, #1650, #19943, #21383, NAMING c.12811 (encoding), NAMING c.530 strict (base-inherited), NAMING c.971 strict (0 re-ping). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(translation,#21391): test_check_pair_count_declared setup_class path Windows hardcode -> dynamique Le setup_class TestAcceptance utilisait Path(r"D:\CoursIA-2") qui est un chemin Windows hardcode. Sur un runner CI Linux, ce chemin n'existe pas (Errno 2 FileNotFoundError PosixPath('D:\CoursIA-2')). Fix : Path(__file__).resolve().parents[3] pour remonter du fichier test au repo root (scripts/translation/tests -> 3 niveaux de parents). NAMING c.91 / c.17071 strict : encage les tokens bloquants. NAMING c.16866 ★★ OK : pre-commit OK (encoding='utf-8' sur subprocess). NAMING c.11064 strict : paths: scripts/translation/** only. Tests : 25/25 PASSED localement (acceptance + integration + helpers). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(translation,#21391): derive constant line in ROUGE msg, address Hermes F1/F2 F2 -- _rouge_message no longer hardcodes :731 (the constant has already drifted to :737). _constant_line_number_in_head resolves the current line from the head text; on failure it prints the search pattern instead of a stale number. New witness asserts the resolved line == the live line and != the stale 731. F1 -- wiring stays the dispatcher's decision (unchanged); the body reformulation is delivered in a follow-up comment on the PR. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Grain: DEEP/notebook-lean — lane myia-ai-01:CoursIA-2 — prev: MED/tooling #19786
Résumé
Pli 2 de l'Epic Origami #19898, issue #20184 : le carnet
ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb(FR) + sibling_en, exécutés avec outputs, etCheck.lean(point d'entrée de vérification du lac, hors globs de la lib). S'appuie sur le commit lac de la même branche (13ac1be :Sensitivity/Sens2026.lean+_en+ imports aux racines) — les deux commits forment le livrable complet du pli.Baseline nav-chain : les 2 findings
Lean-12b/Lean-12c(unreachable, reclassement entree->non-entree par liens de citation croisee) sont ajoutes au baseline dans la PR (commit 9763e6a, +10/-0, garde verte sur branche) -- arbitrage coordinateur #19076 du 2026-10-11, c.6114582529 (option b pour ces 2 entrees ; l'option (a), statut d'entree calcule intra-serie, portee par une PR tooling separee).Fichiers
MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb(nouveau, 29 cellules)MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb(nouveau, markdown traduit, code identique — convention ANALYSE-09_en)MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Check.lean(nouveau, hors globs — même rôle quekls_lean/Check.leanpour le carnet 05)Sensitivity/Sens2026.lean+Sens2026_en.lean+ imports racinesB. Lean — preuve de progrès vérifiable
scripts/lean/count_code_sorry.py --json --lake, champdistinct_code_sorry:files: 19,distinct_code_sorry: 0files: 22,distinct_code_sorry: 0(delta = Sens2026 + _en + Check.lean ; le compteur est exécuté dans le carnet, cellule 6, sortie committée)Build completed successfully (3025 jobs), rc = 0, sortie committée ;lean-sensitivity.ymlrejoue le build en CI..github/workflows/lean-sensitivity.ymlappellelean-axiom.ymlavectarget-modules: "*"(liste dérivée au runtime de la marche du lac) →Sensitivity.Sens2026couvert automatiquement ; les_ensont exclus par design du gate (byte-parité FR/EN des preuves). In-notebook : 7 ×#print axioms=[propext, Classical.choice, Quot.sound]— zérosorryAx, zéronative_decide.Notebooks — preuve d'exécution réelle
execution_count1-10, 0 erreur, 0 cellule code sans output.raise NotImplementedError/assert False/1/0absents) : les 3 exercices sont des stubs C.1 (return None,print("Exercice a completer")), exécutés sans erreur dans le carnet committé.# Solution.## Diagnostic dérive: non applicable (notebooks neufs, aucune sortie réalignée).Verdicts SOTA (attendus par l'issue)
lake buildréel (WSL, toolchain v4.33.0),lake env lean Check.leanréel, mesures Python exactes (stdlib), aucune sortie de substitution nulle part.lake/leansont invoqués pour ce qu'ils sont (build + vérification d'axiomes), pas comme contournement.tribes32, séparations locales — faits,#print axiomsci-dessus).Mesures clés (exactes, re-exécutables, toutes committées dans le carnet)
decide, chiffre à chiffre : s(0)=0, s(impair)=3, bs(0)=3 pourtribes32;or3bs(0)=3 ;orOfAndsbs(0)=2 exact (le lac prouve seulement >0 — la mesure dépasse le théorème, sain).Statuts épistémiques (Epic #19898)
Familles 127/132/186/192 citées « formalisées en amont (
lean/docs/NNN.md) » ; la séparation superquadratique d'Aaronson (= famille 132) citée en regard de nosSeparations.leanavec le statut de veille Pli 1 : préprint non relu par des experts humains à ce jour. Jamais « OpenAI a prouvé X, donc X ». La table des 3 statuts (formalisée / non formalisée / nôtre) est reproduite dans le carnet (§8).README du dossier ANALYSE
Différé volontairement au merge de #20371 (PR ouverte de po-2024 touche le README du même dossier) — garde L898 anti-collision.
Part of #19898
Closes #20184
🤖 Generated with Claude Code